Skip to content

Refactor Data.List.Relation.Binary.Permutation.* #2317

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Draft
wants to merge 65 commits into
base: master
Choose a base branch
from
Draft

Refactor Data.List.Relation.Binary.Permutation.* #2317

wants to merge 65 commits into from

Conversation

@jamesmckinna
Copy link
Contributor

@jamesmckinna jamesmckinna commented Mar 12, 2024 •
edited
Loading

WORK IN PROGRESS: do not review!

Of independent interest to the various competing proposals in #2311 for the 'right' representation, as it attempts to decouple the main properties of the relation from any particular notion. In particular, the isolation of the dependencies (and improved implementation UPDATED can't seem to get the syntax declarations to work for the specialised Propositional version of PermutationReasoning!?) of the Reasoning module, together with a 'better' smart constructor for transitivity in the current implementation(s), as well as a lot of nitpicky streamlining.

NEW: have removed all dependency on well-founded induction on steps in favour of a (structurally inductive proof of) better ↭-split lemma which uses the fact that Permutation R absorbs Pointwise R steps provided R is Transitive.

Currently in DRAFT, but aims to, and is most of the way towards:

  • redefining Propositional as the setoid instance of Setoid, ditto. Properties
  • refactoring Setoid and Setoid.Properties to localise all uses of induction on the Homogeneous representation to properties proved in general in Homogeneous (thereby allowing alternative representations)
  • back-porting lemmas and proofs from Propositional to Setoid or even Homogeneous, incl.
  • I have managed to get hacky/kludge proofs to work, but there is something more systematic to investigate about the higher-dimensional structure of proofs about Pointwise and Permutation lurking offstage...!?

Outstanding issues:

TODO:

  • CHANGELOG ;-)
  • last missing implementations from Propositional (some fiddliness here, plus some deprecation opportunities once things have been suitably generalised) UPDATED only
 ↭-map-inv : List.map f xs ↭′ vs → ∃ λ ys → vs ≡ List.map f ys × xs ↭ ys

remains

  • refactor Homogeneous into Core/Base and Properties (currently a total ⟪casino⟫, esp. wrt dependencies)
  • refactor Setoid.Properties into Core (representation dependent; to be discussed as the best way to achieve such modularisation for (each of) the representation(s)) and Properties depending on that component
  • exporting induction principles while keeping constructors hidden?

Etc. To be continued...

@jamesmckinna jamesmckinna marked this pull request as draft March 12, 2024 08:27
@jamesmckinna jamesmckinna mentioned this pull request Mar 12, 2024
Closed
Taneb
Taneb reviewed Mar 12, 2024
View reviewed changes
This was referenced Mar 16, 2024
Merged
Draft
@jamesmckinna
Copy link
Contributor Author

jamesmckinna commented Mar 26, 2024 •
edited
Loading

Note to self: typechecking appears not to terminate for Data.List.Relation.Binary.Permutation.Homogeneous.Properties!?

Refactored to lift out the lemmas as ...Homogeneous.Properties.HigherDimensional...

@jamesmckinna
Copy link
Contributor Author

jamesmckinna commented Mar 27, 2024 •
edited
Loading

Stopping here as much of the refactoring of (the properties of Setoid as instances of those of) Homogeneous is fairly settled now. So I'll now attempt to retrofit that analysis back onto the old versions. See #2333 for a start.

@jamesmckinna jamesmckinna mentioned this pull request Mar 28, 2024
Merged
@jamesmckinna
Copy link
Contributor Author

jamesmckinna commented Mar 28, 2024 •
edited
Loading

Previously @MatthewDaggitt wrote

Before I review this, am I right in understanding there's really two changes here? Firstly moving lots of stuff from Setoid to Heterogeneous and secondly changing the implementation of Propositional to use Setoid.

If so then could we do this in two different PRs? In particular the second PR is big breaking change, and therefore there are questions about when it exactly it can be merged in.

Please now consider a possible roadmap as follows:

  • (Part I) reconcile the APIs for Propositional and Setoid in their 'old' versions Refactor Data.List.Relation.Binary.Permutation.*, part I #2333 ; this is slightly more conservative, and doesn't even go as far as moving everything to Homogeneous as here
  • (Part II) refactor via Homogeneous.Properties.* and Propositional.Properties and Setoid.Properties in terms of Core (based on Homogeneous) and 'derived' based on the respective Core properties (and refocus this PR on such work)
  • (Part III) revisit [ fix #1354 ] Refactoring Permutation.Propositional #1761 to then reconcile the two definitions, and with minimised Cores via the pattern synonym tricks?

@MatthewDaggitt
Copy link
Contributor

Stopping here

Does this mean the draft status should be removed and this PR reviewed?

@jamesmckinna
Copy link
Contributor Author

Stopping here

Does this mean the draft status should be removed and this PR reviewed?

Thanks @MatthewDaggitt for the prompt to return to this. I think the short answer, for the time being, is/ought to be "No":

  • merge conflicts ahead of of the v2.1 release are stymying various open PRs, including the first part of this, namely Refactor Data.List.Relation.Binary.Permutation.*, part I #2333 , which is badged as v2.2
  • the above (re-)factorisation into three parts, the first of which above, I had hoped made clear that this PR would (eventually ;-)) get broken up, part-by-part, and I haven't had the brain space to return to the second and/or third parts given that they are (potentially) breaking, and moreover, somewhat depend on the eventual fate of the first...

Sound OK to you?

@MatthewDaggitt
Copy link
Contributor

Yes, sounds reasonable.

@jamesmckinna jamesmckinna mentioned this pull request Jun 3, 2025
Merged
@JacquesCarette
Copy link
Contributor

@jamesmckinna if you had help (i.e. someone who could follow your directions on how to push this forward), would you be able to continue work on this?

@jamesmckinna
Copy link
Contributor Author

@jamesmckinna if you had help (i.e. someone who could follow your directions on how to push this forward), would you be able to continue work on this?

Thanks for the offer! now that #2726 has been merged, there may be a clearer path to a (more radical) approach, because both versions (Setoid and Propositional) can delegate to a version (Algorithmic or Declarative) in which the refl behaviour can be better handled. But it now requires someone (else?) to stand back, and get a better global picture of where we are, and a vision of where we want to go... which might end up being breaking, so v3.0?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@Taneb Taneb Taneb left review comments

@MatthewDaggitt MatthewDaggitt MatthewDaggitt left review comments

At least 1 approving review is required to merge this pull request.

Assignees

No one assigned

Labels

addition breaking dependencies discussion refactoring

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@jamesmckinna @MatthewDaggitt @JacquesCarette @Taneb